| Definitions | P   Q,  x:A. B(x),  , s = t,  b,  A, x:A  B(x), P & Q, P  Q, Unit, left + right, Void, False, A  B,  , {x:A| B(x)} , w-knum(w;i;k;t), n+m, es-kind-index(es;k;e), E, Knd, FairFifo, World, Id, a < b, i  j , -n, n - m,  , a(i;t), isnull(a),  , x:A  B(x), #$n, kind(a), a = b,  b, p  q, if b then t else f fi ,  x.A(x), f(a), sum(f(x) | x < k), s ~ t, <a, b>, ES(the_w), first(e), E, t  T,  x. t(x), t.2, Type, t.1, es-pred?(es), time(e), {T}, SQType(T), {i..j }, S  T, suptype(S; T), i j < k, n * m, P Q, pred(e),  x:A. B(x),  x:A.B(x), Top, loc(e), w-pred(w;e), pred(e), Atom$n, kind(e), True,  T, es_info(es) |